/*
 * Kodkod -- Copyright (c) 2005-present, Emina Torlak
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
 * THE SOFTWARE.
 */
package kodkod.instance;

import java.util.AbstractSet;
import java.util.Collection;
import java.util.Iterator;

import kodkod.util.ints.IntIterator;
import kodkod.util.ints.IntSet;
import kodkod.util.ints.Ints;

/**
 * Represents a set of {@link kodkod.instance.Tuple tuples} of a given arity,
 * constructed over a given {@link kodkod.instance.Universe universe}. All
 * polymorphic methods throw a ClassCastException when passed an element that is
 * not a Tuple. All methods throw a NullPointerException when passed null. The
 * iterator of a TupleSet returns tuples in the order of their
 * {@link kodkod.instance.Tuple#index() indeces}.
 *
 * @specfield tuples: set Tuple
 * @specfield universe: Universe
 * @specfield arity: int
 * @invariant tuples.arity = arity && tuples.universe = universe
 * @author Emina Torlak
 */
public final class TupleSet extends AbstractSet<Tuple> implements Cloneable {

    private final Universe universe;
    private final int      arity;
    private final IntSet   tuples;
    private IntSet         indexView = null;

    /**
     * Constructs an empty tuple set for storing tuples of the specified arity, over
     * the given universe.
     *
     * @ensures this.universe' = universe && this.arity' = arity && no this.tuples'
     * @throws NullPointerException universe = null
     * @throws IllegalArgumentException arity < 1
     */
    TupleSet(Universe universe, int arity) {
        if (arity < 1)
            throw new IllegalArgumentException("arity < 1");
        universe.factory().checkCapacity(arity);
        this.universe = universe;
        this.arity = arity;
        tuples = Ints.bestSet(capacity());
    }

    /**
     * Constructs a tuple set of the given arity, over the specified universe, which
     * initially contains all tuples whose indeces are between fromIndex and
     * toIndex, inclusive.
     *
     * @ensures this.universe' = universe && this.arity' = arity && this.tuples' =
     *          {t: Tuple | t.universe=universe && t.arity=arity &&
     *          fromIndex()<=t.index()<=toIndex() }
     * @throws NullPointerException universe = null
     * @throws IllegalArgumentException arity < 1 ||
     * @throws IndexOutOfBoundsException fromIndex !in [0..toIndex] || toIndex !in
     *             [0..universe.size()^arity - 1]
     */
    TupleSet(Universe universe, int arity, int fromIndex, int toIndex) {
        this(universe, arity);
        checkRange(toIndex, 0, capacity() - 1);
        checkRange(fromIndex, 0, toIndex);
        for (int i = fromIndex; i <= toIndex; i++) {
            tuples.add(i);
        }
    }

    /**
     * Returns a set of the given arity that contains all tuples whose indeces are
     * contained in the given int set. Throws an IllegalArgumentException if the set
     * contains an index that is either negative or greater than
     * this.universe.size()^arity - 1. An attempt to iterate over a tuple set backed
     * by an invalid index set will result in a runtime exception.
     *
     * @return {s: TupleSet | s.universe = this.universe && s.arity = arity &&
     *         s.tuples = {t: Tuple | t.index() in tupleIndeces} }
     * @throws NullPointerException tupleIndeces = null
     * @throws IllegalArgumentException arity < 1
     * @throws IllegalArgumentException tupleIndeces.min() < 0 || tupleIndeces.max()
     *             >= this.universe.size()^arity
     */
    TupleSet(Universe universe, int arity, IntSet tupleIndeces) {
        if (arity < 1)
            throw new IllegalArgumentException("arity < 1");
        universe.factory().checkCapacity(arity);
        this.universe = universe;
        this.arity = arity;
        if (!tupleIndeces.isEmpty()) {
            if (tupleIndeces.min() < 0 || tupleIndeces.max() >= capacity())
                throw new IllegalArgumentException(tupleIndeces.min() + "<0 || " + tupleIndeces.max() + ">=" + universe.size() + "^" + arity);
        }
        tuples = tupleIndeces;
    }

    /**
     * Copy constructor.
     *
     * @ensures constructs a deep copy of the given tupleset
     */
    private TupleSet(TupleSet original) {
        this.universe = original.universe;
        this.arity = original.arity;
        try {
            this.tuples = original.tuples.clone();
        } catch (CloneNotSupportedException e) {
            throw new InternalError(); // unreachable code
        }
        this.indexView = null;
    }

    /**
     * Throws an IndexOutOfBoundsException if index is not in [min..max]
     */
    private final void checkRange(int index, int min, int max) {
        if (index < min || index > max)
            throw new IndexOutOfBoundsException(index + " !in " + "[" + min + ".." + max + "]");
    }

    /**
     * Returns the capacity of this set -- the maximum number of tuples that it can
     * hold, given its universe and arity.
     *
     * @return this.universe.size() ^ this.arity
     */
    public final int capacity() {
        return (int) StrictMath.pow(universe.size(), arity);
    }

    /**
     * Returns this.universe.
     *
     * @return this.universe
     */
    public Universe universe() {
        return universe;
    }

    /**
     * Returns this.arity
     *
     * @return this.arity
     */
    public int arity() {
        return arity;
    }

    /**
     * Returns an unmodifiable int set view of the tuples stored in this set.
     * Specifically, the returned int set contains an integer i iff this set
     * contains a tuple with the index i. The view is backed by this set, so changes
     * to this set are reflected in the index set.
     *
     * @return { s: IntSet | s.ints = {i: int | some t: this.tuples | t.index = i}
     */
    public IntSet indexView() {
        if (indexView == null) {
            indexView = Ints.unmodifiableIntSet(tuples);
        }
        return indexView;
    }

    /**
     * Returns an unmodifiable view of the this tupleset. This method allows modules
     * to provide "read-only" access to internal tuple sets. Query operations on the
     * returned set "read through" to the specified set, and attempts to modify the
     * returned set, whether direct or via its iterator, result in an
     * UnsupportedOperationException.
     *
     * @return an unmodifiable view of the this tupleset
     */
    public TupleSet unmodifiableView() {
        return new TupleSet(universe, arity, indexView());
    }

    /**
     * Returns a tuple set that is the cross product of this and the specified set.
     *
     * @return {t: TupleSet | t.arity = this.arity + s.arity && t.universe =
     *         this.universe && t.tuples = this.tuples->s.tuples }
     * @throws NullPointerException s = null
     * @throws IllegalArgumentException s.universe != this.universe
     */
    public TupleSet product(TupleSet s) {
        if (!s.universe().equals(universe))
            throw new IllegalArgumentException("s.universe != this.universe");
        final TupleSet ret = new TupleSet(universe, arity + s.arity());
        if (!s.isEmpty()) {
            final int mCapacity = (int) StrictMath.pow(universe.size(), s.arity);
            for (IntIterator indeces0 = tuples.iterator(); indeces0.hasNext();) {
                int i0 = mCapacity * indeces0.next();
                for (IntIterator indeces1 = s.tuples.iterator(); indeces1.hasNext();) {
                    ret.tuples.add(i0 + indeces1.next());
                }
            }
        }
        return ret;
    }

    /**
     * Projects this TupleSet onto the given dimension.
     *
     * @return {s: TupleSet | s.arity = 1 && s.universe = this.universe && s.tuples
     *         = { t: Tuple | some q: this.tuples | q.atoms[dimension] =
     *         t.atoms[int] } }
     * @throws IllegalArgumentException dimension < 0 || dimension >= this.arity
     */
    public TupleSet project(int dimension) {
        if (dimension < 0 || dimension >= arity) {
            throw new IllegalArgumentException("dimension < 0 || dimension >= this.arity");
        }
        final IntSet projection = Ints.bestSet(universe.size());
        final TupleFactory factory = universe.factory();
        for (IntIterator indexIter = tuples.iterator(); indexIter.hasNext();) {
            projection.add(factory.project(indexIter.next(), arity, dimension));
        }
        return new TupleSet(universe, 1, projection);
    }

    /**
     * Returns a deep copy of this tuple set.
     *
     * @return {s: TupleSet - this | s.universe = this.universe && s.tuples =
     *         this.tuples }
     */
    @Override
    public TupleSet clone() {
        // ok to use a copy constructor to clone a final class
        return new TupleSet(this);
    }

    /**
     * Returns an iterator over the tuples in this tupleset.
     *
     * @return an iterator over the tuples in this tupleset.
     */
    @Override
    public Iterator<Tuple> iterator() {
        return new Iterator<Tuple>() {

            IntIterator indexIter = tuples.iterator();

            @Override
            public boolean hasNext() {
                return indexIter.hasNext();
            }

            @Override
            public Tuple next() {
                return universe.factory().tuple(arity, indexIter.next());
            }

            @Override
            public void remove() {
                indexIter.remove();
            }
        };
    }

    /**
     * Returns the index of the given tuple, if the tuple has the same arity and
     * universe as this. Otherwise throws an IllegalArgumentException.
     *
     * @return t.index
     * @throws IllegalArgumentException t.arity != this.arity || t.universe !=
     *             this.universe
     */
    private final int extractIndex(Tuple t) {
        if (t.arity() != arity || !t.universe().equals(universe)) {
            throw new IllegalArgumentException("t.arity != this.arity || t.universe != this.universe");
        }
        return t.index();
    }

    /**
     * Returns true if this contains the given object.
     *
     * @return o in this.tuples
     * @throws IllegalArgumentException o.arity != this.arity || o.universe !=
     *             this.universe
     */
    @Override
    public boolean contains(Object o) {
        return tuples.contains(extractIndex((Tuple) o));
    }

    /**
     * Returns the size of this tupleset.
     *
     * @return #this.tuples
     */
    @Override
    public int size() {
        return tuples.size();
    }

    /**
     * Removes all tuples from this tupleset.
     *
     * @ensures no this.tuples'
     */
    @Override
    public void clear() {
        tuples.clear();
    }

    /**
     * Adds the specified tuple to this tupleset. Returns true if this set was
     * changed as the result of the operation.
     *
     * @ensures this.tuples' = this.tuples + t
     * @return o !in this.tuples
     * @throws IllegalArgumentException t.universe != this.universe || t.arity !=
     *             this.arity
     */
    @Override
    public boolean add(Tuple t) {
        return tuples.add(extractIndex(t));
    }

    /**
     * Removes the given object from this tupleset, if present, and returns true.
     * Otherwise does nothing and returns false.
     *
     * @ensures this.tuples' = this.tuples - o
     * @return o in this.tuples
     * @throws IllegalArgumentException o.universe != this.universe || o.arity !=
     *             this.arity
     */
    @Override
    public boolean remove(Object o) {
        return tuples.remove(extractIndex((Tuple) o));
    }

    /**
     * If c is not a TupleSet or it is a tupleset with a universe different than
     * this.universe, returns null. Otherwise, returns the tuples associated with
     * the modifiable view of c.
     *
     * @requires c in TupleSet => c.arity = this.arity
     * @return c in TupleSet && c.universe = this.universe && c.arity = this.arity
     *         => c.tuples, null
     * @throws NullPointerException s = null
     * @throws IllegalArgumentException this.arity!=s.arity
     */
    private IntSet extractTuples(Collection< ? > c) {
        if (c instanceof TupleSet) {
            final TupleSet s = (TupleSet) c;
            if (arity != s.arity())
                throw new IllegalArgumentException("this.arity!=c.arity");
            return universe.equals(s.universe()) ? s.tuples : null;
        }
        return null;
    }

    /**
     * Returns true if this contains all tuples from c. Otherwise returns false.
     *
     * @return c.elements in this.tuples
     * @throws IllegalArgumentException some t: c.elements | t.universe !=
     *             this.universe || t.arity != this.arity
     */
    @Override
    public boolean containsAll(Collection< ? > c) {
        final IntSet cTuples = extractTuples(c);
        return cTuples == null ? super.containsAll(c) : tuples.containsAll(cTuples);
    }

    /**
     * Adds all tuples from c to this, if not present, and returns true. Otherwise
     * does nothing and returns false.
     *
     * @ensures this.tuples' = this.tuples + c.elements
     * @return c.elements !in this.tuples
     * @throws IllegalArgumentException some t: c.elements | t.universe !=
     *             this.universe || t.arity != this.arity
     */
    @Override
    public boolean addAll(Collection< ? extends Tuple> c) {
        final IntSet cTuples = extractTuples(c);
        return cTuples == null ? super.addAll(c) : tuples.addAll(cTuples);
    }

    /**
     * Removes all tuples in c from this, if present, and returns true. Otherwise
     * does nothing and returns false.
     *
     * @ensures this.tuples' = this.tuples - c.elements
     * @return some c.elements & this.tuples
     * @throws IllegalArgumentException some t: c.elements | t.universe !=
     *             this.universe || t.arity != this.arity
     */
    @Override
    public boolean removeAll(Collection< ? > c) {
        final IntSet cTuples = extractTuples(c);
        return cTuples == null ? super.removeAll(c) : tuples.removeAll(cTuples);
    }

    /**
     * Removes all tuples from this that are not in c, if any, and returns true.
     * Otherwise does nothing and returns false.
     *
     * @ensures this.tuples' = this.tuples & c.elements
     * @return this.tuples !in c.elements
     * @throws IllegalArgumentException some t: c.elements | t.universe !=
     *             this.universe || t.arity != this.arity
     */
    @Override
    public boolean retainAll(Collection< ? > c) {
        final IntSet cTuples = extractTuples(c);
        return cTuples == null ? super.retainAll(c) : tuples.retainAll(cTuples);
    }

    /**
     * Returns true if o contains the same tuples as this.
     *
     * @return this.tuples = o.elements
     */
    @Override
    public boolean equals(Object o) {
        if (this == o)
            return true;
        if (o instanceof TupleSet) {
            final TupleSet s = (TupleSet) o;
            return arity == s.arity && universe.equals(s.universe) && tuples.equals(s.tuples);
        }
        return super.equals(o);
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public int hashCode() {
        return tuples.hashCode();
    }
}
